a, b:. a  b  -(b)  -(a) 

latex

Definitions	T, r - s, x. t(x), {T}, True, P  Q, P  Q, P  Q, P & Q, , t  T, t.2, t.1, q_le(r;s), , x f y, <+>, a  b, r  s, P  Q, x:A. B(x), x(s), S  T
Lemmas	qadd comm q, qinv inv q, bool wf, true wf, squash wf, assert-qeq, or functionality wrt iff, assert of bor, iff transitivity, iff functionality wrt iff, all functionality wrt iff, qadd wf, int inc rationals, qmul wf, qeq wf2, qsub wf, qpositive wf, bor wf, assert wf, iff wf, rationals wf